Inference at * 
Iof proof for Lemma fseg nil:


  T:Type, L:(T List). fseg(T;L;[])  (null(L)) 

latex

 by ((Unfold `fseg` 0) 
CollapseTHEN (ObviousListInduction)) 

latex

C.

Definitions

, T, , #$n, Void, tt, , True, t  T, False, (xL.P(x)), xL. P(x), A c B, a < b, a <p b, a  b, a ~ b, b | a, Dec(P), P  Q, left + right, P  Q, P  Q, x:AB(x), P & Q, x:A  B(x), fseg(T;L1;L2), P  Q, x:A. B(x), x:A. B(x), Y, x.A(x), Type, p q, p  q, p  q, b, [d], a < b, x f y, a < b, x =a y, (i = j), i z j, i <z j, p =b q, null(as), A, b, ||as||, s ~ t, [car / cdr], rec-case(a) of [] => s | x::y => z.t(x;y;z), [], as @ bs, f(a), type List, s = t

Lemmas

append wf, assert of null, iff wf, not wf, bool wf, null wf, squash wf, true wf, btrue wf, decidable assert, rev implies wf, assert wf